State of the art computerized components are very complex and require extensive quality assurance checks. One of the commonly used techniques is formal verification in which the computerized component is modeled and is examined by a model checker. The model describes all possible behaviors of the computerized component based on inputs from the environment and calculations performed by the computerized component itself. Most components are represented by cycled models in which the state of the component may differ from one cycle to the other. It will be noted that the computerized component may be a software component, firmware component, hardware component or the like. It will be further noted that in some cases the component to be verified may be a business method, user interaction, communication protocol or any other form of activity or computation that may be expressed formally using a model.
A model checker checks that the model holds a predetermined specification property. An exemplary specification property may be that a triggered event is always handled by the component or that a certain variable is never assigned a predetermined value. The specification property may be attributed to one or more cycles. For simplicity, the current disclosure discusses mainly a specification property that is associated to a cycle. However, it should be understood that the disclosed subject matter is not limited to such a specification property. For example, the specification property may be associated with more than one cycle, such as for example, after a flag is raised in a cycle, an alert is issued within a predetermined number of cycles. In some exemplary embodiments, the property is what is known in the art as safety property, and may be provided using a Property Specification Language (PSL) formula such as AGp, indicating that Always (i.e., in each cycle), Globally (i.e. in each possible scenario), property p holds. Property p may be a property provided in temporal logic.
One form of model checking utilizes a Bounded Model Checker (BMC). The bounded model checker determines whether the specification property holds for a predetermined number of cycles. A bounded model is a model which has a bounded number of cycles. A bounded model associated with an unbounded model may be determined by truncating behaviors of the model in every cycle that exceeds a predetermined bound. While the BMC may falsify the specification property by determining that in a given one or more cycles the specification property is not held, it cannot prove that the specification is held for the model, as the number of cycles is bounded. The BMC can only provide a proof that the specification is held for every cycle within the predetermined number of cycles.
One family of BMC engines utilizes a Boolean satisfiability problem solver, also known as SAT solver, for solving a Boolean satisfiability problem that is associated with the predetermined number of cycles. The Boolean satisfiability problem is formulated in a Conjunctive Normal Form (CNF) formula. A CNF formula of the form ITRK may describe a behavior of the bounded model within k steps. I is the initial state, TR is a transition relation from state i to state i+1, k transition relations are utilized to model behavior until cycle k. In some cases, in order to verify the property p, the CNF may correspond to a formula ITRKp. In case a satisfying assignment of the CNF is found, the property p is falsified. Otherwise, that SAT solver may prove that there are no satisfying assignments to the CNF. Optionally, the SAT solver may provide a proof of unsatisfiability.